Kind-deq  EqDecider(Knd) 

latex

Definitions	t  T, Knd, Kind-deq, x:A. B(x)
Lemmas	union-deq wf, IdLnk wf, Id wf, product-deq wf, idlnk-deq wf, id-deq wf